p:FinProbSpace, n:, X:RandomVariable(p;n). E(n;X)   

latex

Definitions

, t  T, x:AB(x), x:A. B(x), ||as||, #$n, {i..j}, Type, {x:A| B(x)} , , a < b, s = t, False, A, A  B, x:A  B(x), P & Q, i  j < k, RandomVariable(p;n), P  Q, Void, Outcome, l[i], x. t(x), a  j < b. E(j), type List, FinProbSpace, <a, b>, , rv-shift(x;X), x.A(x), E(n;F), weighted-sum(p;F), , , A  B, x,y:A//B(x;y), if b then t else f fi , EquivRel(T;x,y.E(x;y)), tt, qeq(r;s), , x,y. t(x;y), f(a), b, b, (i = j), P  Q, Unit, left + right, null, , i  j , -n, n+m, n - m

Lemmas

ge wf, nat properties, nat wf, null-seq wf, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert of eq int, eq int wf, bnot wf, not wf, assert wf, int-rational, quotient wf, bool wf, qeq wf2, btrue wf, b-union wf, int nzero wf, weighted-sum wf, rv-shift wf, qsum wf, select wf, int inc rationals, le wf, int seg wf, length wf1, rationals wf